Termination w.r.t. Q proof of TRS/currying/AG01#3.10.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

Q is empty.

↳ QTRS

  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

Q is empty.

The TRS is overlay and locally confluent. By [15] we can switch to innermost.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(rm, n)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(filter2, app'(f, x)), f), x)
APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(app'(eq, x), y)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(add, app'(f, x)), app'(app'(map, f), xs))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(app, app'(app'(rm, n), x)), y)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(add, n), y)
APP'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, m), x))
APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(add, n), x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(if_rm, app'(app'(eq, n), m)), n)
APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(rm, n)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(rm, n), x)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(min, app'(app'(add, n), x))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(filter2, app'(f, x)), f)
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(le, n)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(eq, n)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(filter, f)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(minsort, app'(app'(app, app'(app'(rm, n), x)), y))
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(add, m), app'(app'(rm, n), x))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(filter2, app'(f, x))
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(add, n), app'(app'(app, x), y))
APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x))))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(add, app'(f, x))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app, app'(app'(rm, n), x))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(map, f), xs)
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(filter, f)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(add, x)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(minsort, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(app, x), y)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(minsort, x), app'(app'(add, n), y))
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(if_rm, app'(app'(eq, n), m))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(eq, x)
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app, x)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(rm, n)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(if_min, app'(app'(le, n), m))
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(add, x), app'(app'(filter, f), xs))
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(eq, n)
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(eq, n), app'(min, app'(app'(add, n), x)))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(le, n), m)
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(app'(le, x), y)
APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, n), x))
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(le, x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(eq, n), m)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(rm, n)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(filter2, app'(f, x)), f), x)
APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(app'(eq, x), y)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(add, app'(f, x)), app'(app'(map, f), xs))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(app, app'(app'(rm, n), x)), y)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(add, n), y)
APP'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, m), x))
APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(add, n), x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(if_rm, app'(app'(eq, n), m)), n)
APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(rm, n)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(rm, n), x)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(min, app'(app'(add, n), x))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(filter2, app'(f, x)), f)
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(le, n)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(eq, n)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(filter, f)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(minsort, app'(app'(app, app'(app'(rm, n), x)), y))
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(add, m), app'(app'(rm, n), x))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(filter2, app'(f, x))
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(add, n), app'(app'(app, x), y))
APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x))))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(add, app'(f, x))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app, app'(app'(rm, n), x))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(map, f), xs)
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(filter, f)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(add, x)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(minsort, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(app, x), y)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(minsort, x), app'(app'(add, n), y))
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(if_rm, app'(app'(eq, n), m))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(eq, x)
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app, x)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(rm, n)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(if_min, app'(app'(le, n), m))
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(add, x), app'(app'(filter, f), xs))
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(eq, n)
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(eq, n), app'(min, app'(app'(add, n), x)))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(le, n), m)
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(app'(le, x), y)
APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, n), x))
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(le, x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(eq, n), m)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We deleted some edges using various graph approximations

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(rm, n)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(filter2, app'(f, x)), f), x)
APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(app'(eq, x), y)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(add, app'(f, x)), app'(app'(map, f), xs))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(app, app'(app'(rm, n), x)), y)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(add, n), y)
APP'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, m), x))
APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(add, n), x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(if_rm, app'(app'(eq, n), m)), n)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(rm, n), x)
APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(rm, n)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(min, app'(app'(add, n), x))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(filter2, app'(f, x)), f)
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(le, n)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(eq, n)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(filter, f)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(minsort, app'(app'(app, app'(app'(rm, n), x)), y))
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(add, m), app'(app'(rm, n), x))
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(filter2, app'(f, x))
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(add, n), app'(app'(app, x), y))
APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x))))
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(add, app'(f, x))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app, app'(app'(rm, n), x))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(map, f), xs)
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(filter, f)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(add, x)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(minsort, x)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(minsort, x), app'(app'(add, n), y))
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(app, x), y)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(if_rm, app'(app'(eq, n), m))
APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(eq, x)
APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app, x)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(rm, n)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(if_min, app'(app'(le, n), m))
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(eq, n)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(add, x), app'(app'(filter, f), xs))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(eq, n), app'(min, app'(app'(add, n), x)))
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(app'(filter, f), xs)
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(le, n), m)
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(app'(le, x), y)
APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, n), x))
APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x))
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil)
APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(le, x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(eq, n), m)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 7 SCCs with 37 less nodes.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(app, x), y)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13]. Here, we combined the reduction pair processor with the A-transformation [14] which results in the following intermediate Q-DP Problem.
Q DP problem:
The TRS P consists of the following rules:

APP(add(n, x), y) → APP(x, y)

R is empty.
The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.

The following pairs can be oriented strictly and are deleted.

APP'(app'(app, app'(app'(add, n), x)), y) → APP'(app'(app, x), y)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
APP(x1, x2) = x1
add(x1, x2) = add(x2)

Lexicographic Path Order [19].
Precedence:

trivial

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(app'(le, x), y)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

LE(s(x), s(y)) → LE(x, y)

R is empty.
The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.

The following pairs can be oriented strictly and are deleted.

APP'(app'(le, app'(s, x)), app'(s, y)) → APP'(app'(le, x), y)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
LE(x1, x2) = x2
s(x1) = s(x1)

Lexicographic Path Order [19].
Precedence:

trivial

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, n), x))
APP'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, m), x))
APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

MIN(add(n, add(m, x))) → IF_MIN(le(n, m), add(n, add(m, x)))
IF_MIN(false, add(n, add(m, x))) → MIN(add(m, x))
IF_MIN(true, add(n, add(m, x))) → MIN(add(n, x))

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.

The following pairs can be oriented strictly and are deleted.

APP'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, n), x))
APP'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → APP'(min, app'(app'(add, m), x))

The remaining pairs can at least be oriented weakly.

APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))

Used ordering: Combined order from the following AFS and order.
MIN(x1) = x1
add(x1, x2) = add(x2)
IF_MIN(x1, x2) = x2

Lexicographic Path Order [19].
Precedence:

trivial

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(min, app'(app'(add, n), app'(app'(add, m), x))) → APP'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 0 SCCs with 1 less node.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(app'(eq, x), y)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

EQ(s(x), s(y)) → EQ(x, y)

R is empty.
The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.

The following pairs can be oriented strictly and are deleted.

APP'(app'(eq, app'(s, x)), app'(s, y)) → APP'(app'(eq, x), y)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
EQ(x1, x2) = x2
s(x1) = s(x1)

Lexicographic Path Order [19].
Precedence:

trivial

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

RM(n, add(m, x)) → IF_RM(eq(n, m), n, add(m, x))
IF_RM(true, n, add(m, x)) → RM(n, x)
IF_RM(false, n, add(m, x)) → RM(n, x)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)
map(x0, nil)
map(x0, add(x1, x2))
filter(x0, nil)
filter(x0, add(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.

The following pairs can be oriented strictly and are deleted.

APP'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)
APP'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → APP'(app'(rm, n), x)

The remaining pairs can at least be oriented weakly.

APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))

Used ordering: Combined order from the following AFS and order.
RM(x1, x2) = x2
add(x1, x2) = add(x2)
IF_RM(x1, x2, x3) = x3

Lexicographic Path Order [19].
Precedence:

trivial

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(rm, n), app'(app'(add, m), x)) → APP'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 0 SCCs with 1 less node.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(minsort, app'(app'(add, n), x)), y) → APP'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
APP'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → APP'(app'(minsort, x), app'(app'(add, n), y))
APP'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → APP'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(app'(map, f), xs)
APP'(app'(app'(app'(filter2, true), f), x), xs) → APP'(app'(filter, f), xs)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(map, f), app'(app'(add, x), xs)) → APP'(f, x)
APP'(app'(filter, f), app'(app'(add, x), xs)) → APP'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
APP'(app'(app'(app'(filter2, false), f), x), xs) → APP'(app'(filter, f), xs)

The TRS R consists of the following rules:

app'(app'(eq, 0), 0) → true
app'(app'(eq, 0), app'(s, x)) → false
app'(app'(eq, app'(s, x)), 0) → false
app'(app'(eq, app'(s, x)), app'(s, y)) → app'(app'(eq, x), y)
app'(app'(le, 0), y) → true
app'(app'(le, app'(s, x)), 0) → false
app'(app'(le, app'(s, x)), app'(s, y)) → app'(app'(le, x), y)
app'(app'(app, nil), y) → y
app'(app'(app, app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(app, x), y))
app'(min, app'(app'(add, n), nil)) → n
app'(min, app'(app'(add, n), app'(app'(add, m), x))) → app'(app'(if_min, app'(app'(le, n), m)), app'(app'(add, n), app'(app'(add, m), x)))
app'(app'(if_min, true), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, n), x))
app'(app'(if_min, false), app'(app'(add, n), app'(app'(add, m), x))) → app'(min, app'(app'(add, m), x))
app'(app'(rm, n), nil) → nil
app'(app'(rm, n), app'(app'(add, m), x)) → app'(app'(app'(if_rm, app'(app'(eq, n), m)), n), app'(app'(add, m), x))
app'(app'(app'(if_rm, true), n), app'(app'(add, m), x)) → app'(app'(rm, n), x)
app'(app'(app'(if_rm, false), n), app'(app'(add, m), x)) → app'(app'(add, m), app'(app'(rm, n), x))
app'(app'(minsort, nil), nil) → nil
app'(app'(minsort, app'(app'(add, n), x)), y) → app'(app'(app'(if_minsort, app'(app'(eq, n), app'(min, app'(app'(add, n), x)))), app'(app'(add, n), x)), y)
app'(app'(app'(if_minsort, true), app'(app'(add, n), x)), y) → app'(app'(add, n), app'(app'(minsort, app'(app'(app, app'(app'(rm, n), x)), y)), nil))
app'(app'(app'(if_minsort, false), app'(app'(add, n), x)), y) → app'(app'(minsort, x), app'(app'(add, n), y))
app'(app'(map, f), nil) → nil
app'(app'(map, f), app'(app'(add, x), xs)) → app'(app'(add, app'(f, x)), app'(app'(map, f), xs))
app'(app'(filter, f), nil) → nil
app'(app'(filter, f), app'(app'(add, x), xs)) → app'(app'(app'(app'(filter2, app'(f, x)), f), x), xs)
app'(app'(app'(app'(filter2, true), f), x), xs) → app'(app'(add, x), app'(app'(filter, f), xs))
app'(app'(app'(app'(filter2, false), f), x), xs) → app'(app'(filter, f), xs)

The set Q consists of the following terms:

app'(app'(eq, 0), 0)
app'(app'(eq, 0), app'(s, x0))
app'(app'(eq, app'(s, x0)), 0)
app'(app'(eq, app'(s, x0)), app'(s, x1))
app'(app'(le, 0), x0)
app'(app'(le, app'(s, x0)), 0)
app'(app'(le, app'(s, x0)), app'(s, x1))
app'(app'(app, nil), x0)
app'(app'(app, app'(app'(add, x0), x1)), x2)
app'(min, app'(app'(add, x0), nil))
app'(min, app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, true), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(if_min, false), app'(app'(add, x0), app'(app'(add, x1), x2)))
app'(app'(rm, x0), nil)
app'(app'(rm, x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, true), x0), app'(app'(add, x1), x2))
app'(app'(app'(if_rm, false), x0), app'(app'(add, x1), x2))
app'(app'(minsort, nil), nil)
app'(app'(minsort, app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, true), app'(app'(add, x0), x1)), x2)
app'(app'(app'(if_minsort, false), app'(app'(add, x0), x1)), x2)
app'(app'(map, x0), nil)
app'(app'(map, x0), app'(app'(add, x1), x2))
app'(app'(filter, x0), nil)
app'(app'(filter, x0), app'(app'(add, x1), x2))
app'(app'(app'(app'(filter2, true), x0), x1), x2)
app'(app'(app'(app'(filter2, false), x0), x1), x2)

We have to consider all minimal (P,Q,R)-chains.